10/17/2008 Lesson Plan

Citizenship axioms:

- What are the entities in the domain?

- What are the predicates?

- What are the axioms?

Discuss alternatives to each.

------------------

Midterm review: hand out sheet and discuss.

------------------

First-order inference: Unification and Lifting

A x . man(x) => mortal(x)
man(socretes).
 therefore: mortal(socretes).

In propositional logic: would have to instatiate the axioms over the set of all men
-- billions of people!
Instead: want to determine just what to substitute for x that is needed to prove
mortal(socretes).

In this case, it is easy: substitute socretes for x, write this as {x/socretes}

Two literals L1 and L2 UNIFY if there a substition THETA such L1 THETA = L2 THETA
In this case:
        motal(socretes) {x/socretes} = mortal(x) {x/socretes}

If two literals unify, they have a MOST GENERAL UNIFIER (substitution)

Say: L1 = Loves(x, mother(x))
     L2 = Loves(John, y)

What is substitution that makes L1 and L2 the same?
     {x/John, y/mother(John)}a           

Can generalize Modus Ponens to use unification:

   p1', p2', ..., pn', (p1 & p2 & ... & pn => q)
   ---------------------------------------------
                      q THETA

*if* there is a subsitution THETA such that
    p1' THETA = p1
    p2' THETA = p2 
    ...
    p3' THETA = p3

Details of the unification (MGU) algorithm:
Works on LISP notation.
Singleton: a constant, predicate, or variable.

Unify(x, y, THETA) 
// given partial substitution THETA, return a substition that
// makes x and y the same

  if (x and y are singletons and x=y) then return THETA;
  if (x is a variable) then 
     if there is a substitution x/z in THETA then
	return Unify(z,y,THETA)
     else
	return THETA U {x/y};
  if (y is a variable) then 
     if there is a substitution y/z in THETA then
	return Unify(x,z,THETA)
     else
	return THETA U {y/x};
  if (x or y is a singleton) then FAIL;
  // so both x and y are lists, the first element of the
  // list is either a predicate or a functor
  if ( first(x) != first(y) ) then fail
  for each argument a1,...,an in x and a1',...,an' in y do:
      THETA = Unify(ai,ai', THETA);
  return THETA
end.